//this is the precondition for sum
/*@ n>=0 && n<5
 */
int sum (int n)
{
  int s, i;
  array[5, int] *a;

  i=0;
  s=3;
  if(i<=n) 
  {
    (*a)[3] = s+1;
    (*a)[2] = 1;
  }
  return (*a)[2];
}
/*@  result == 1
 */
//this is the post-condition for sum

